COMMENT ⊗   VALID 00005 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	Ideas for exam questions
C00005 00003	Readin
C00006 00004	WRITIN
C00007 00005	PROVIN
C00009 ENDMK
C⊗;
Ideas for exam questions

Ideas:[MFB]
design a representation of floating point numbers which includes
two pieces of information: a mantissa (integer), and an exponent (base 10) (integer).
Using this representation write programs to add, subtract, multiply, divide,
exponentiate, and compare two complex numbers. (Using functions on integers)

Simiilar for fractions, complex numbers.

How about bignums? 

Rewrite:[CLT]
Let ⊗rules be a list of "rewriting rules" of the form $$(EQUAL lhs rhs)$.
The $lhs and $rhs components of the rule may have ``pattern variables'' in them.
We say that $lhs matches ⊗e if there is a list of substitutions that can be 
made for the pattern variables in $lhs such that the resulting instantiation
is equal to ⊗e.  
A rule ⊗r is applicable to ⊗e if the $lhs part of ⊗r matches some subexpression
of ⊗e.  Applying ⊗r to ⊗e then consists of replacing that subexpression by
the instantiation of $rhs corresponding to the list of substitutions that 
caused $lhs to match at this point.

The program ⊗rewrite[e,rules] goes through the list of rules and looks for
one that is applicable to ⊗e.  If one is found it is applied,
and rewrite is applied again to the "simplified" expression using the
same set of rules. If no applicable rules are found ⊗e is returned.



Write interpreter for flograph programs: takes pgm and interpretation of symbols 
and input for pgm.  Computes output.

Readin

WRITIN
PROVIN

Representation of hereditarily finite sets (of atoms) and operations thereon.
	set-equality, union, pairing, difference,
	list of KPU axioms to be satisfied

#.  Show that ⊗mapcar commutes with ⊗reverse and ⊗append.  Officially we don't
have a way to reason about programs taking functions as arguments.  However,
if we replace ⊗mapcar by a function schema, ⊗mapper, involving a function 
parameter ⊗F, then we can give a proof schema, which will provide a proof
for any particular instance of ⊗mapper obtained by choosing a particular function 
for ⊗F.  Thus 

⊗⊗⊗∀u.mapper u=qif qn u qthen qNIL qelse [F qa u_._mapper[qd u]]⊗

and you are to prove
.begin nofill

##. ⊗⊗∀u v.[mapper u*v=mapper u*mapper v]⊗
##. ⊗⊗∀u.[mapper reverse u=reverse mapper u]⊗
.end


IMPURE

sequential prog→rec defn
	fn for each statement
	optimize on second pass
recursion removal:
	fringe→flat→flatagin for example
Iterative program→prog

modify program to return more infor about what it did

inplace reverse

convert f[x]←qt[f,x] to ff[x,n]←if n=0 then error else qt[λx.ff[x,n-1],x]